Do not turn trivially diverging loops into assume(false) #3223
Conversation
CBMC's symbolic execution by default turns `while(true) {}` loops into
`assume(false)` to counter trivial non-termination of symbolic
execution. When unwinding assertions are enabled, however, we should
report the non-termination of such loops.
|
Thanks @tautschnig for the quick fix! Should we consider this a soundness issue in CBMC and fix it on the CBMC side instead? i.e., when unwinding assertions are enabled, self loops should not be replaced with |
I think we should indeed seek to make this consistent on the CBMC side for version 6. I'll come up with a PR. |
|
Yes, when applying loop contracts, lack of decreases may lead to vacuous verification, which is the case of Zyad's comment. Now the synthesizer for Kani doesn't synthesize decrease clauses, and should does before it became stable. |
@tautschnig if we fix this on version 6, we do not need to merge this PR, correct? Shall we close it in favor of the new update? |
Merging this PR would help disentangle a Kani issue from the CBMC release. Once CBMC v6 is released and Kani starts using it we can then remove this, but then we will anyway end up removing several options from the command line being used to invoke CBMC. |
CBMC's symbolic execution by default turns
while(true) {}loops intoassume(false)to counter trivial non-termination of symbolic execution. When unwinding assertions are enabled, however, we should report the non-termination of such loops.Resolves: #2909
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.